ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da).
(eclrepeat?(x))  (eclrepeat-a(x)  ecl(ds;da)) 

latex

Definitions	x. t(x), if b then t else f fi , tt, ff, eclrepeat-a(x), t  T, eclrepeat?(x), b, P  Q, ecl(ds;da), x:A. B(x), x(s), False, eclcatch(a;l), eclthrow(a;n), a.n, [a]*, eclor(a;b), ecland(a;b), eclseq(a;b), , eclbase(k;test)
Lemmas	Id wf, Knd wf, fpf wf, ecl wf, eclrepeat? wf, assert wf, true wf, false wf